    \section{M\'odulo Diccionario Trie}

    Modulo que se explica con TAD Diccionario(String, $\alpha$), este modulo no ofrece los servicios Borrar y Claves.

	\subsection{Interfaz}
	
\begin{interfaces}
    {DiccionarioTrie}
    {$\alpha$}
    {$\alpha$}
    {String, Bool}
    {Diccionario(string, $\alpha$)}
    {diccTrie($\alpha$)}

    \interfaz{Vacio}{}{diccTrie($\alpha$)}
			{true} 
			{res = Vacio}
			{\complejidad{$\Theta$}{1}}{}
			{}
			{Crea un diccionario vacio}
			
    \interfaz{Definir}{\parametro{in/out}{d}{diccTrie($\alpha$)}, \parametro{in}{c}{string}, \parametro{in}{s}{$\alpha$}}{}
			{$d_0$ = $d$} 
			{d = Definir(c, s, d)}
			{\complejidad{$\Theta$}{$|c| + \text{copy}(\alpha)$}}{}
			{}
			{Define una nueva clave $d$ con el valor $c$}


    \interfaz{Definido?}{\parametro{in}{d}{diccTrie($\alpha$)}, \parametro{in}{c}{string}}{bool}
		    {true} 
		    {res = Def?(c, d)}
		    {\complejidad{O}{$|c|$ + copy($\alpha$)}}{}
		    {}
		    {Devuelve true si hay un valor definido para la clave $c$}
		    
    \interfaz{Obtener}{\parametro{in}{d}{diccTrie($\alpha$)}, \parametro{in}{c}{string}}{$\alpha$}
		    {Def?(d, c)} 
		    {res = Obtener(c, d)}
		    {\complejidad{$\Theta$}{$|c|$}}{}
		    {El resultado tiene aliasing con el elemento del diccionario.}
		    {Devuelve el valor definido para la clave $c$}
			
\end{interfaces}			

	\subsection{Representaci\'on}
	
    \representacion{diccTrie($\alpha$)}{se representa con}{nodoDicc},
      donde \representacion{nodoDicc}{es}{}
    \begin{definicionTupla}
    \elementoTupla{proximasLetras}{arreglo\_estatico[27] de puntero(nodoDicc))},\\
	\elementoTupla{elemento}{puntero($\alpha$)}\\
    \end{definicionTupla}

	\subsection{Algoritmos}
	
    \begin{codebox}
    \encabezadoFuncion{iDefinido?}{\parametro{in}{d}{nodoDicc}, \parametro{in}{c}{string}}{bool}\\
	\li $i \gets 0$
	\li $pNodo \gets \&d$
	\li	\While $(i < |c|) \land (pNodo \neq NULL)$
	\li	\Do
			$char \gets numeroDeCaracterEn(c, i)$
    \li		$pNodo \gets (*pNodo).proximasLetras[char]$	
	\li		$i \gets i + 1$
		\End
    
	\li	$res \gets ((pNodo \neq NULL) \land ((*pNodo).elemento \neq NULL))$
	\end{codebox}
	
	
	La complejidad es claramente $O(|c|)$, pues son todas operaciones $O(1)$, y el ciclo esta acotado por el largo de la clave.
	
    \begin{codebox}
	\encabezadoFuncion{iObtener}{\parametro{in}{d}{nodoDicc}, \parametro{in}{c}{string}}{$\alpha$}\\
	\li $i \gets 0$
	\li $pNodo \gets \&d$
	\li	\While $(i < |c|)$
	\li	\Do
			$char \gets numeroDeCaracterEn(c, i)$
    \li		$pNodo \gets (*pNodo).proximasLetras[char]$	
	\li		$i \gets i + 1$
		\End
    
	\li	$res \gets *((*pNodo).elemento)$
	\end{codebox}
	La complejidad es claramente $\Theta(|c|)$, pues son todas operaciones $O(1)$, y el ciclo siempre se ejecuta $|c|$ veces.
	
    \begin{codebox}
	\encabezadoFuncion{iVacio}{}{nodoDicc}\\
	\li $i \gets 0$
	\li $res \gets nodoDicc$
	\li $res.elemento \gets NULL$
	\li	\While $(i < 27)$
	\li	\Do
    		$res.proximasLetras[i] \gets NULL$	
	\li		$i \gets i + 1$
		\End
	\end{codebox}
	La complejidad es $O(1)$, pues solo crea el nodoDicc y asigna todos los punteros en NULL, lo cual siempre lleva la misma cantidad de operaciones.
	
	\begin{codebox}
	\encabezadoFuncion{iDefinir}{\parametro{in/out}{d}{nodoDicc}, \parametro{in}{c}{string}, \parametro{in}{s}{$\alpha$}}{}\\
	\li $i \gets 0$
	\li $pNodo \gets \&d$
	\li	\While $(i < |c|)$
	\li	\Do
			$char \gets numeroDeCaracterEn(c, i)$
    \li		$tmpNodo \gets (*pNodo).proximasLetras[char]$
   	\li		\If $tmpNodo = NULL$
	\li		\Then
                $j \gets 0$
    \li         $(*pNodo).proximasLetras[char] \gets \&nodoDicc$
	\li         $tmpNodo \gets (*pNodo).proximasLetras[char]$
	\li         $(*tmpNodo).elemento \gets NULL$ 
	
	\li         \While $(j < 27)$
	\li         \Do
                    $(*tmpNodo).proximasLetras[j] \gets NULL$
    \li             $j \gets j + 1$
                \End
            \End
    \li     $pNodo \gets tmpNodo$            
	\li		$i \gets i + 1$
		\End
    
    \li	$(*pNodo).elemento \&copy(s)$
	\end{codebox}
    La complejidad es $O(|c| + copy(s))$. Los pasos anteriores al ciclo son claramente $O(1)$. El cliclo externo (linea 3) realiza exactamente $|c|$ iteraciones, cada una $O(1)$, pues son todas opraciones $O(1)$ y el ciclo interno (linea 11) realiza exactamente 27 operaciones, por lo que es $O(1)$. Por \'ultimo se hace un llamado a $copy(\alpha)$, cuya complejidad dependera del $\alpha$ en cuesti\'on.

    \subsection{Invariante de representaci\'on}
    
    Con la implementaci\'on elegida, todo diccionario es valido siempre y cuando este no tenga ciclos, por lo que el invariante de representaci\'on solo debe encargarse de chequear esto.
    
    $Rep : nodoDicc \longrightarrow bool$\\
    \indent $Rep(n) \equiv sinRepetidos(\&n, Ag(\&n, \emptyset))$\\


    $sinRepetidos(nodop, conj) \equiv (*nodop).proximasLetras[0] \notin proximoConj(nodop, conj) - (*nodop).proximasLetras[0] \land 
        \indent \indent sinRepetidos((*nodop).proximasLetras[0], proximoConj(nodop, conj)) \land ... \land \\
        \indent \indent (*nodop).proximasLetras[26] \notin proximoConj(nodop, conj) - (*nodop).proximasLetras[26] \land \\
        \indent \indent sinRepetidos((*nodop).proximasLetras[26], proximoConj(nodop, conj))$\\
   
    $proximoConj(nodop, conj) \equiv Ag((*nodop).proximasLetras[0], Ag(..., Ag((*nodop).proximasLetras[26], conj)...))$\\

    \subsection{Funci\'on de abstracci\'on}
    
    $Abs : nodoDicc \longrightarrow dicc(string, \alpha)$\\
    \indent $Abs(n) \equiv d \ / \ (\forall s:string) definido(d, s) \Leftrightarrow estaDefinido(n, s) \land definido(d, s) \Leftarrow (obtener(d, s) = obtenerSignificado(n, s))$\\ 
    
    estaDefinido(n, s) $\equiv$ if s = $""$ then\\
    \indent \indent (n.elemento $\neq$ NULL) \\ 
    \indent else \\
    \indent \indent if n.siguientesLetras[s[0]] = NULL then \\
    \indent \indent \indent false \\
    \indent \indent else \\
    \indent \indent \indent estaDefinido(*(n.siguientesLetras[s[0]]), substr(s, 1, $|s| - 1$) \\
    \indent \indent fi\\
    \indent fi\\
    
    obtenerSignificado(n, s) $\equiv$ if s = $""$ then\\
    \indent \indent n.elemento \\ 
    \indent else \\
    \indent \indent obtenerSignificado(*(n.siguientesLetras[s[0]]), substr(s, 1, $|s| - 1$) \\
    \indent fi\\
